#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "klee_change_macros.h"
#include "klee_change_functions.h"
int lib(int x) {
	if (x < klee_change(0,5))
		return klee_change(0,5);
	else
		return x;
}

int client(int x){
	if (x < 0){
		return -lib((-x)*5)/5;
	}else{
		return lib((x+1)*5)/5 - 1;
	}
}

int main(int argc, char *argv[]) {
  int x= argv[1][0] - '0';

  return client(x);
}
